YES 0.911 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((enumFromTo :: Bool  ->  Bool  ->  [Bool]) :: Bool  ->  Bool  ->  [Bool])

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((enumFromTo :: Bool  ->  Bool  ->  [Bool]) :: Bool  ->  Bool  ->  [Bool])

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
takeWhile p [] = []
takeWhile p (x : xs)
 | p x
 = x : takeWhile p xs
 | otherwise
 = []

is transformed to
takeWhile p [] = takeWhile3 p []
takeWhile p (x : xs) = takeWhile2 p (x : xs)

takeWhile0 p x xs True = []

takeWhile1 p x xs True = x : takeWhile p xs
takeWhile1 p x xs False = takeWhile0 p x xs otherwise

takeWhile2 p (x : xs) = takeWhile1 p x xs (p x)

takeWhile3 p [] = []
takeWhile3 wv ww = takeWhile2 wv ww

The following Function with conditions
toEnum 0 = False
toEnum 1 = True

is transformed to
toEnum wy = toEnum3 wy
toEnum wx = toEnum1 wx

toEnum0 True wx = True

toEnum1 wx = toEnum0 (wx == 1) wx

toEnum2 True wy = False
toEnum2 wz xu = toEnum1 xu

toEnum3 wy = toEnum2 (wy == 0) wy
toEnum3 xv = toEnum1 xv



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ NumRed

mainModule Main
  ((enumFromTo :: Bool  ->  Bool  ->  [Bool]) :: Bool  ->  Bool  ->  [Bool])

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ NumRed
HASKELL
              ↳ Narrow

mainModule Main
  (enumFromTo :: Bool  ->  Bool  ->  [Bool])

module Main where
  import qualified Prelude



Haskell To QDPs